Inference at * 1 1 0 0 
Iof proof for Lemma absval eq:



1. x : 
2. y : 
  (if 0 z x then x else -x fi  = if 0 z y then y else -y fi )  x =  y 

latex

 by PERMUTE{1:n,
 by PERMUTE{2:n,
 by PERMUTE{3:n,
 by PERMUTE{4:n,
 by PERMUTE{5:n,
 by PERMUTE{6:n,
 by PERMUTE{7:n,
 by PERMUTE{8:n,
 by PERMUTE{9:n,
 by PERMUTE{10:n,
 by PERMUTE{11:n,
 by PERMUTE{12:n,
 by PERMUTE{10:n,
 by PERMUTE{13:n,
 by PERMUTE{11:n,
 by PERMUTE{14:n,
 by PERMUTE{15:n,
 by PERMUTE{16:n,
 by PERMUTE{17:n,
 by PERMUTE{18:n,
 by PERMUTE{16:n,
 by PERMUTE{15:n,
 by PERMUTE{19:n} 

latex

 1: .....wf..... NILNIL

 1:   0 z x  
 2: .....wf..... NILNIL

 2:     Type
 3: .....wf..... NILNIL

 3: 3. 0 z x = tt
 3:   (0 z x = tt)  
 4: .....wf..... NILNIL

 4: 3. 0 z x = tt
 4:   (0 z x)  
 5: .....wf..... NILNIL

 5: 3. 0 z x = tt
 5:   (0  x)  
 6: .....wf..... NILNIL

 6: 3. 0 z x = tt
 6:   0 z x  
 7: .....wf..... NILNIL

 7: 3. 0 z x = tt
 7:   0  
 8: .....wf..... NILNIL

 8: 3. 0 z x = tt
 8:   x  
 9: 

 9: 3. 0  x
 9:   (if tt then x else -x fi  = if 0 z y then y else -y fi )  x =  y
 10: .....wf..... NILNIL

 10: 3. 0 z x = ff
 10:   (0 z x = ff)  
 11: .....wf..... NILNIL

 11: 3. 0 z x = ff
 11:   (x <z 0)  
 12: .....wf..... NILNIL

 12: 3. 0 z x = ff
 12:   (x < 0)  
 13: .....wf..... NILNIL

 13: 3. 0 z x = ff
 13:   ((0 z x))  
 14: .....wf..... NILNIL

 14: 3. 0 z x = ff
 14:   0 z x  
 15: .....wf..... NILNIL

 15: 3. 0 z x = ff
 15:   0  
 16: .....wf..... NILNIL

 16: 3. 0 z x = ff
 16:   x  
 17: .....antecedent..... NILNIL

 17: 3. 0 z x = ff
 17:   True
 18: .....wf..... NILNIL

 18: 3. 0 z x = ff
 18: 4. ((0 z x)) = (x <z 0)
 18:    = 
 19: 

 19: 3. x < 0
 19:   (if ff then x else -x fi  = if 0 z y then y else -y fi )  x =  y
 .

Definitions	{x:A| B(x)} , x.A(x), b, i <z j, a < b, ff, inr x , x:A  B(x), b, f(a), A  B, tt, , Ax, inl x , left + right, x:AB(x), Type, i =  j, -n, #$n, i z j, if b then t else f fi , s = t, , , Unit, , True, T, P  Q, P & Q, P  Q, x:A. B(x), t  T, P  Q
Lemmas	assert of lt int, bnot of le int, bool wf, true wf, squash wf, assert wf, eqff to assert, assert of le int, eqtt to assert, iff transitivity